Nuprl Lemma : absval_neg
13,42
postcript
pdf
i
:{...0}. |
i
| = (-
i
)
latex
Up
int
2
,
int
2
Definitions
True
,
ff
,
if
b
then
t
else
f
fi
,
,
tt
,
t
T
,
x
:
A
.
B
(
x
)
,
{...
i
}
Lemmas
int
lower
wf
,
bnot
wf
,
lt
int
wf
,
le
wf
,
assert
wf
,
bool
wf
,
le
int
wf
origin